T:Type, l:(T List), i:, x:T. l[i:=x]  (T List) 

latex

Definitions	t  T, x:A. B(x), ||as||, {i..j}, i  j , P  Q, False, A, A  B, , l[i], (i = j), if b then t else f fi , mklist(n;f), f[x:=v], l[i:=x]
Lemmas	mklist wf, ifthenelse wf, eq int wf, select wf, int seg wf, non neg length, length wf1